Nuprl Lemma : do-apply-mu' 11,40
A:Type, P:(A), d:(x:A. Dec(n:. ((P(x,n))))), x:A.
(can-apply(mu'(P);x))
 {((P(x,do-apply(mu'(P);x)))) & (i:{0..do-apply(mu'(P);x)}. ((P(x,i))))} 
latex

ProofTree

Definitionsb, do-apply(f;x), mu'(P), can-apply(f;x), x:AB(x), P  Q, Type, t  T, , , f(a), x:A. B(x), x:A  B(x), x:A. B(x), Dec(P), Void, x:A.B(x), Top, S  T, left + right, {x:A| B(x)} , suptype(S; T), {i..j}, P & Q, {T}, False, A, p-mu-decider, s ~ t, p-mu(P;x), A c B, if b then t else f fi , True, A  B, , , s = t
Lemmasp-mu-decider, p-mu wf, true wf, false wf, can-apply wf, mu' wf, top wf, decidable wf, assert wf, nat wf, bool wf

origin